#!/usr/bin/ruby -w

require "cnf.rb"
require "sat_parser.rb"

# Converts a formula in DIMACS SAT notation, and converts it to DIMACS CNF
# notation. The source of the formula can either be a string or a file.
class FormulaConverter

  def convert_from_file(sat_file)
    return convert_from_string(IO.read(sat_file))
  end
  
  def convert_from_string(sat_string)
  
  end

  def convert_tree(root)
    puts root.to_s
    root = arrow_free(root)
    root = nnf(root)
    root = cnf(root)
    
    clauses = parse_clauses(root, [])
    # Filter out all clauses that do not have any variable in them
    clauses = clauses.delete_if do |clause|
    	clause.variables.empty?
    end
    
    return CnfFormula.new(clauses)
  end
  
  def parse_clauses(node, clauses)
    if node.kind_of?(Literal)
      if clauses.empty?
        clauses.push(CnfClause.new)
      end
      clauses[-1].add_variable(CnfVariable.new(node.value.to_s, node.kind_of?(NegationLiteral)))
    elsif node.kind_of?(And)
      clauses.push(CnfClause.new)
      parse_clauses(node.left, clauses)
      clauses.push(CnfClause.new)      
      parse_clauses(node.right, clauses)    
    elsif node.kind_of?(Or)
      parse_clauses(node.left, clauses)
      parse_clauses(node.right, clauses)
    else
      raise ArgumentError.new("Unknown type: " + node.to_s)
    end
    
    return clauses
  end
  
  private
  
  # Note: The following methods are taken from the slides

  def arrow_free(token)
    if token.kind_of?(NegationLiteral)
      return NegationLiteral.new(arrow_free(Literal.new(token.value)))
    elsif token.kind_of?(Literal)
      return token
    elsif token.kind_of?(And)
      return And.new(arrow_free(token.left), arrow_free(token.right))
    elsif token.kind_of?(Or)
      return Or.new(arrow_free(token.left), arrow_free(token.right))
    else
      raise StandardError.new("Unexpected token: " + token.to_s)
    end
  end
  
  def nnf(token)
    if token.kind_of?(NegationLiteral)
      if token.value.kind_of?(NegationLiteral)
        return nnf(token.value.value)
      elsif token.value.kind_of?(And)
        neg_left = NegationLiteral.new(token.value.left)
        neg_right = NegationLiteral.new(token.value.right)
        return Or.new(nnf(neg_left), nnf(neg_right))
      elsif token.value.kind_of?(Or)
        neg_left = NegationLiteral.new(token.value.left)
        neg_right = NegationLiteral.new(token.value.right)
        return And.new(nnf(neg_left), nnf(neg_right))
      elsif token.value.kind_of?(Literal)
        return token
      end
    elsif token.kind_of?(Literal)
      return token
    elsif token.kind_of?(And)
      return And.new(nnf(token.left), nnf(token.right))
    elsif token.kind_of?(Or)
      return Or.new(nnf(token.left), nnf(token.right))
    end
    
    raise StandardError.new("Unexpected token: " + token.to_s)
  end
  
  def cnf(token)
    if token.kind_of?(Literal)
      return token
    elsif token.kind_of?(And)
      return And.new(cnf(token.left), cnf(token.right))
    elsif token.kind_of?(Or)
      return dist(cnf(token.left), cnf(token.right))
    else
      raise StandardError.new("Unexpected token: " + token.to_s)
    end
  end
  
  def dist(token1, token2)
    if token1.kind_of?(And)
      return And.new(dist(token1.left, token2), dist(token1.right, token2))
    elsif token2.kind_of?(And)
      return And.new(dist(token1, token2.left), dist(token1, token2.right))
    else
      return Or.new(token1, token2)
    end
  end
end
